$M$.ef($k$,$x$,$s$,$v$)?$w$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$($M$.2.2.2.2).1($<$$k$, $x$$>$)?$\lambda$$s$,$v$. $w$($s$,$v$)